Thanks for the contribution.
max_diffl should rather be called derive1_maxl by the look of existing lemmas.
I pushed force because of a rebase w.r.t. master (to get the changelog right).

Hello, Thank you for you help.
I am currently trying to rework the main proof into a better format

Fact der_max f g x v :
  f x <> g x -> derivable f x v -> derivable g x v ->
  (fun h => h^-1 *: (((f \max g) \o shift x) (h *: v) - (f \max g) x)) @
    0^' --> if f x < g x then 'D_v g x else 'D_v f x.

So that its more general and fits with the library more. Should I redraft this pr or make a new one with an update from this format to the newer better one?

Sorry I made a mistake and merged the wrong branch, should be fixed now.

A few helpful lemmas were added to classical/functions.v which are about order but rely on funext so they can't be in mathcomp order.

Its worth noting that the removal of the dependence on v != 0 many lemmas had in derive.v will lead to incompatibility with previous versions of Analysis

Before all, sincere apologies for the slow reactivity, February has been busy.
Your PR will now be treated quickly.

Sorry I made a mistake and merged the wrong branch, should be fixed now.

No harm!

Its worth noting that the removal of the dependence on v != 0 many lemmas had in derive.v will lead to incompatibility with previous versions of Analysis

Indeed, but this is a strict generalization, so dependencies that will break will be easily fixed and to the benefit of the user. The "Generalized" entry of the changelog should be appropriate to document these changes.

I have updated the changelog and also made a linting pass on the code (a bit of shortening and formatting to abide by the contributing guide https://github.com/math-comp/math-comp/blob/master/CONTRIBUTING.md).

I think that we need to take another look at the naming of lemmas before merging.

Should not we state these properties in terms of (f `|` g)%O instead of f \max g (similarly (f`&`g)%O instead of f \min g)?

Not directly a comment to this PR itself, but \max and \min look bad names (e.g., f \max g can be neither f nor g).

Should not we state these properties in terms of (f `|` g)%O instead of f \max g (similarly (f`&`g)%O instead of f \min g)?

Not directly a comment to this PR itself, but \max and \min look bad names (e.g., f \max g can be neither f nor g).

I don't have an answer (except maybe a comment: I have difficulties to remember which of | and & corresponds to max ^_^) but I recorded these issues as issue #1896 and issue #1897

It might look like I bypassed the rules but the requested change has actually been addressed.